Nuprl Lemma : locl_one_one
0,22
postcript
pdf
a
,
b
:Id. locl(
a
) = locl(
b
)
Knd
a
=
b
latex
Definitions
Id
,
t
T
,
IdLnk
,
Prop
,
P
Q
,
x
:
A
.
B
(
x
)
,
locl(
a
)
,
Knd
Lemmas
IdLnk
wf
,
Id
wf
origin
a, b:Id. locl(a) = locl(b) 
Knd 
a = b a, b:Id. locl(a) = locl(b) Knd a = b T Qx:A. B(x)